Library varignon

Require Import incidence.
Require Import midpoint.

Section Triangle.

Context `{M:triangle_theory}.

Lemma varignon : ∀ A B C D,
  parallel (line (midpoint A B) (midpoint B C)) (line (midpoint C D) (midpoint A D)).
Proof.
intros.
destruct A;destruct B;destruct C;destruct D.
simpl.
ring.
Qed.

End Triangle.